T:Type{i}, S:((T)Prop{i'}). T  generic{i:l}(T; f.S(f))  (f:(T). S(f)) 

latex

Definitions

, x:AB(x), f(a), x(s), x:AB(x), x:A. B(x), x:A. B(x), P & Q, Generic{f:T|S(f)}, Type, t  T, Prop, x. t(x), P  Q, l[i], s = t, ||as||, #$n, {i..j}, type List, a<b, n+m, l1  l2, AB, Void, False, A, , {x:A| B(x) }, i  j < k, nil, car.cdr, as @ bs, 1of(t), i<j, if b t else f fi, x.A(x), primrec(n;b;c), True, ij, b, b, , T, P  Q, P  Q, Unit, left+right, i=j, {T}, SQType(T), s ~ t, n-m, ij, -n, P  Q, Dec(P), A & B

Lemmas

iseg select, decidable le, decidable int equal, select wf, length append, length wf2, iseg length, ge wf, nat properties, iseg transitivity, iseg append, iseg weakening, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, not wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, bool wf, bnot wf, assert wf, le int wf, primrec wf, ifthenelse wf, lt int wf, pi1 wf, append wf, int seg wf, iseg wf, length wf1, le wf, generic wf, nat wf